/*
 * The Elephant Reasoner
 *
 * Copyright (C) Baris Sertkaya (sertkaya.baris@gmail.com)
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */


#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <pthread.h>

#include "../model/datatypes.h"
#include "../model/model.h"
#include "../model/utils.h"
#include "../model/limits.h"
#include "../utils/stack.h"
#include "../index/utils.h"
#include "../hashing/key_hash_table.h"
#include "../hashing/key_value_hash_table.h"
#include "utils.h"
#include "saturation_worker.h"

// for statistics
extern int saturation_unique_subsumption_count, saturation_total_subsumption_count;
extern int saturation_unique_link_count, saturation_total_link_count;

extern pthread_mutex_t scheduled_concepts_mutex;
/*
 * Saturates the scheduled axioms of a given concept.
 * Returns:
 * 	-1: If the KB is inconsistent. In this case it immediately returns, i.e., saturation process
 * 	is cancelled.
 * 	0: Otherwise
 */
void* saturation_worker(void* worker_data) {

	// set the tbox to the one in the worker_data
	TBox* tbox = ((struct saturation_worker_data*) worker_data)->tbox;
	// set the scheduled_concepts to the one in the worker data
	Stack* scheduled_concepts = &(((struct saturation_worker_data*) worker_data)->scheduled_concepts);

	printf("Saturation worker starting: %lu\n", pthread_self());

	pthread_mutex_lock(&(scheduled_concepts_mutex));
	Concept* scheduled_concept = pop(scheduled_concepts);
	if (scheduled_concept != NULL)
		scheduled_concept->is_scheduled = 0;
	pthread_mutex_unlock(&(scheduled_concepts_mutex));

	while (scheduled_concept != NULL) {

		// first pop from the scheduled axioms
		ConceptSaturationAxiom* ax = pop(&(scheduled_concept->scheduled_axioms));


		// if there is no scheduled axiom, pop from the foreign axioms
		if (ax == NULL) {
			pthread_mutex_lock(&(scheduled_concept->foreign_axioms_mutex));
			ax = pop(&(scheduled_concept)->foreign_axioms);
			pthread_mutex_unlock(&(scheduled_concept->foreign_axioms_mutex));
		}

		/*
		printf("Worker: %lu => ", pthread_self());
		print_concept(scheduled_concept);
		printf("\n");
		*/

		int i, j, k;
		while (ax != NULL) {

		if (ax->lhs != scheduled_concept)
			printf("differ!\n");
			switch (ax->type) {
			case SUBSUMPTION_CONJUNCTION_INTRODUCTION:
			case SUBSUMPTION_EXISTENTIAL_INTRODUCTION:
				++saturation_total_subsumption_count;
				// no conjunction decomposition, no existential decomposition and no bottom rule here
				if (MARK_CONCEPT_SATURATION_AXIOM_PROCESSED(ax)) {
					++saturation_unique_subsumption_count;

					// printf("SUBS:");
					// print_concept(ax->lhs);
					// printf("->");
					// print_concept(ax->rhs);
					// printf("\n");

					// pthread_mutex_lock(&(ax->lhs->subsumer_list_mutex));
					add_to_concept_subsumer_list(ax->lhs, ax->rhs);
					// pthread_mutex_unlock(&(ax->lhs->subsumer_list_mutex));

					// conjunction introduction
					// the first conjunct
					for (i = 0; i < ax->rhs->first_conjunct_of_count; i++) {
						// check if lhs is subsumed by the second conjunct as well
						if (IS_SUBSUMED_BY(ax->lhs, ax->rhs->first_conjunct_of_list[i]->description.conj->conjunct2))
							// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->first_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
							push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->first_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
					}

					// now the same for the second conjunct
					for (i = 0; i < ax->rhs->second_conjunct_of_count; i++) {
						// check if lhs is also subsumed by the first conjunct
						if (IS_SUBSUMED_BY(ax->lhs, ax->rhs->second_conjunct_of_list[i]->description.conj->conjunct1))
							// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->second_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
							push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->second_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
					}

					// existential introduction
					Concept* ex;
					for (i = 0; i < ax->lhs->predecessor_r_count; ++i)
						for (j = 0; j < ax->lhs->predecessors[i]->role->subsumer_count; ++j) {
							ex = GET_NEGATIVE_EXISTS(ax->rhs, ax->lhs->predecessors[i]->role->subsumer_list[j]);
							if (ex != NULL)
								for (k = 0; k < ax->lhs->predecessors[i]->filler_count; ++k) {
									pthread_mutex_lock(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms_mutex));
									push(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms), create_concept_saturation_axiom(ax->lhs->predecessors[i]->fillers[k], ex, NULL, SUBSUMPTION_EXISTENTIAL_INTRODUCTION));
									pthread_mutex_unlock(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms_mutex));

									// push ax->lhs->predecessors[i]->fillers[k] to the scheduled_concepts
									pthread_mutex_lock(&(scheduled_concepts_mutex));
									if (ax->lhs->predecessors[i]->fillers[k]->is_scheduled == 0) {
										push(scheduled_concepts, ax->lhs->predecessors[i]->fillers[k]);
										ax->lhs->predecessors[i]->fillers[k]->is_scheduled = 1;
									}
									pthread_mutex_unlock(&(scheduled_concepts_mutex));
								}
						}


					// told subsumers
					for (i = 0; i < ax->rhs->told_subsumer_count; i++)
						// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->told_subsumers[i], NULL, SUBSUMPTION_TOLD_SUBSUMER));
						push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->told_subsumers[i], NULL, SUBSUMPTION_TOLD_SUBSUMER));
				}
				break;
			case SUBSUMPTION_INITIALIZATION:
			case SUBSUMPTION_CONJUNCTION_DECOMPOSITION:
			case SUBSUMPTION_TOLD_SUBSUMER:
			case SUBSUMPTION_BOTTOM:
				++saturation_total_subsumption_count;
				// all here
				if (MARK_CONCEPT_SATURATION_AXIOM_PROCESSED(ax)) {
					++saturation_unique_subsumption_count;

					add_to_concept_subsumer_list(ax->lhs, ax->rhs);

					// printf("SUBS:");
					// print_concept(ax->lhs);
					// printf("->");
					// print_concept(ax->rhs);
					// printf("\n");

					// bottom rule
					if (ax->rhs == tbox->bottom_concept) {
						// If the top concept or a nominal is subsumed by bottom, the kb is inconsistent
						if (ax->lhs->type == NOMINAL || ax->lhs == tbox->top_concept)
							// return inconsistent immediately
							// return (void*) -1;
							pthread_exit((void*) -1);
						// We push the saturation axiom bottom <= ax->lhs, if we already know ax->lhs <= bottom. This way ax->lhs = bottom
						// gets computed. The information bottom <= c is not taken into account for any other concept c.
						pthread_mutex_lock(&(tbox->bottom_concept->foreign_axioms_mutex));
						push(&(tbox->bottom_concept->foreign_axioms), create_concept_saturation_axiom(tbox->bottom_concept, ax->lhs, NULL, SUBSUMPTION_BOTTOM));
						pthread_mutex_unlock(&(tbox->bottom_concept->foreign_axioms_mutex));

						// push bottom to the scheduled_concepts
						pthread_mutex_lock(&(scheduled_concepts_mutex));
						if (tbox->bottom_concept->is_scheduled == 0) {
							push(scheduled_concepts, tbox->bottom_concept);
							tbox->bottom_concept->is_scheduled = 1;
						}
						pthread_mutex_unlock(&(scheduled_concepts_mutex));

						for (i = 0; i < ax->lhs->predecessor_r_count; ++i)
							for (j = 0; j < ax->lhs->predecessors[i]->filler_count; ++j) {
								pthread_mutex_lock(&(ax->lhs->predecessors[i]->fillers[j]->foreign_axioms_mutex));
								push(&(ax->lhs->predecessors[i]->fillers[j]->foreign_axioms), create_concept_saturation_axiom(ax->lhs->predecessors[i]->fillers[j], tbox->bottom_concept, NULL, SUBSUMPTION_BOTTOM));
								pthread_mutex_unlock(&(ax->lhs->predecessors[i]->fillers[j]->foreign_axioms_mutex));

								// push ax->lhs->predecessors[i]->fillers[j] to the scheduled_concepts
								pthread_mutex_lock(&(scheduled_concepts_mutex));
								if (ax->lhs->predecessors[i]->fillers[j]->is_scheduled == 0) {
									push(scheduled_concepts, ax->lhs->predecessors[i]->fillers[j]);
									ax->lhs->predecessors[i]->fillers[j]->is_scheduled = 1;
								}
								pthread_mutex_unlock(&(scheduled_concepts_mutex));
							}
					}


					// conjunction introduction
					// the first conjunct
					for (i = 0; i < ax->rhs->first_conjunct_of_count; i++) {
						// check if lhs is subsumed by the second conjunct as well
						if (IS_SUBSUMED_BY(ax->lhs, ax->rhs->first_conjunct_of_list[i]->description.conj->conjunct2))
							// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->first_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
							push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->first_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
					}

					// now the same for the second conjunct
					for (i = 0; i < ax->rhs->second_conjunct_of_count; i++) {
						// check if lhs is also subsumed by the first conjunct
						if (IS_SUBSUMED_BY(ax->lhs, ax->rhs->second_conjunct_of_list[i]->description.conj->conjunct1))
							// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->second_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
							push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->second_conjunct_of_list[i], NULL, SUBSUMPTION_CONJUNCTION_INTRODUCTION));
					}

					switch (ax->rhs->type) {
					case CONJUNCTION:
						// conjunction decomposition
						// conjunct 1 as rhs
						// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.conj->conjunct1, NULL, SUBSUMPTION_CONJUNCTION_DECOMPOSITION));
						push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.conj->conjunct1, NULL, SUBSUMPTION_CONJUNCTION_DECOMPOSITION));

						// conjunct 2 as rhs
						// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.conj->conjunct2, NULL, SUBSUMPTION_CONJUNCTION_DECOMPOSITION));
						push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.conj->conjunct2, NULL, SUBSUMPTION_CONJUNCTION_DECOMPOSITION));
						break;
					case EXISTENTIAL_RESTRICTION:
						// existential decomposition
						// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.exists->filler, ax->rhs->description.exists->role, SUCCESSOR_LINK));
						push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->description.exists->filler, ax->rhs->description.exists->role, SUCCESSOR_LINK));

						pthread_mutex_lock(&(ax->rhs->description.exists->filler->foreign_axioms_mutex));
						push(&(ax->rhs->description.exists->filler->foreign_axioms), create_concept_saturation_axiom(ax->rhs->description.exists->filler, ax->lhs, ax->rhs->description.exists->role, PREDECESSOR_LINK));
						pthread_mutex_unlock(&(ax->rhs->description.exists->filler->foreign_axioms_mutex));

						// push ax->rhs->description.exists->filler to the scheduled_concepts
						pthread_mutex_lock(&(scheduled_concepts_mutex));
						if (ax->rhs->description.exists->filler->is_scheduled == 0) {
							push(scheduled_concepts, ax->rhs->description.exists->filler);
							ax->rhs->description.exists->filler->is_scheduled = 1;
						}
						pthread_mutex_unlock(&(scheduled_concepts_mutex));

						break;
					}

					// existential introduction
					int j,k;
					Concept* ex;
					for (i = 0; i < ax->lhs->predecessor_r_count; ++i)
						for (j = 0; j < ax->lhs->predecessors[i]->role->subsumer_count; ++j) {
							ex = GET_NEGATIVE_EXISTS(ax->rhs, ax->lhs->predecessors[i]->role->subsumer_list[j]);
							if (ex != NULL)
								for (k = 0; k < ax->lhs->predecessors[i]->filler_count; ++k) {
									pthread_mutex_lock(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms_mutex));
									push(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms), create_concept_saturation_axiom(ax->lhs->predecessors[i]->fillers[k], ex, NULL, SUBSUMPTION_EXISTENTIAL_INTRODUCTION));
									pthread_mutex_unlock(&(ax->lhs->predecessors[i]->fillers[k]->foreign_axioms_mutex));

									/*
									// push ax->lhs->predecessors[i]->fillers[k] to the scheduled_concepts
									pthread_mutex_lock(&(scheduled_concepts_mutex));
									push(scheduled_concepts, ax->lhs->predecessors[i]->fillers[k]);
									pthread_mutex_unlock(&(scheduled_concepts_mutex));
									*/
								}
						}


					// told subsumers
					for (i = 0; i < ax->rhs->told_subsumer_count; i++)
						// push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->told_subsumers[i], NULL, SUBSUMPTION_TOLD_SUBSUMER));
						push(&(ax->lhs->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ax->rhs->told_subsumers[i], NULL, SUBSUMPTION_TOLD_SUBSUMER));
				}
				break;
			case PREDECESSOR_LINK:
				++saturation_total_link_count;
				break;
				if(add_predecessor(ax->lhs, ax->role, ax->rhs, tbox)) {
					++saturation_unique_link_count;

					// bottom rule
					if (IS_SUBSUMED_BY(ax->lhs, tbox->bottom_concept)) {
						pthread_mutex_lock(&(ax->rhs->foreign_axioms_mutex));
						push(&(ax->rhs->foreign_axioms), create_concept_saturation_axiom(ax->rhs, tbox->bottom_concept, NULL, SUBSUMPTION_BOTTOM));
						pthread_mutex_unlock(&(ax->rhs->foreign_axioms_mutex));

						/*
						// push ax->rhs to the scheduled_concepts
						pthread_mutex_lock(&(scheduled_concepts_mutex));
						push(scheduled_concepts, ax->rhs);
						pthread_mutex_unlock(&(scheduled_concepts_mutex));
						*/
					}

					// existential introduction
					for (i = 0; i < ax->lhs->subsumer_count; ++i)
						for (j = 0; j < ax->role->subsumer_count; ++j) {
							Concept* ex = GET_NEGATIVE_EXISTS(ax->lhs->subsumer_list[i], ax->role->subsumer_list[j]);
							if (ex != NULL) {
								pthread_mutex_lock(&(ax->rhs->foreign_axioms_mutex));
								push(&(ax->rhs->foreign_axioms), create_concept_saturation_axiom(ax->rhs, ex, NULL, SUBSUMPTION_EXISTENTIAL_INTRODUCTION));
								pthread_mutex_unlock(&(ax->rhs->foreign_axioms_mutex));

								/*
								// push ax->rhs to the scheduled_concepts
								pthread_mutex_lock(&(scheduled_concepts_mutex));
								push(scheduled_concepts, ax->rhs);
								pthread_mutex_unlock(&(scheduled_concepts_mutex));
								*/
							}
						}

					// now the same for the successors of the filler of the existential on the rhs
					// the role composition where this role appears as the first component
					for (i = 0; i < ax->role->first_component_of_count; ++i) {

						// printf("role composition where this role appears as the first component: ");
						// print_role(ax->rhs->description.exists->role->subsumer_list[i]->first_component_of_list[j]);
						// printf("\n");

						for (j = 0; j < ax->lhs->successor_r_count; ++j)
							if (ax->lhs->successors[j]->role == ax->role->first_component_of_list[i]->description.role_composition->role2) {
								for (k = 0; k < ax->lhs->successors[j]->filler_count; ++k) {
									pthread_mutex_lock(&(ax->rhs->foreign_axioms_mutex));
									push(&(ax->rhs->scheduled_axioms),
											create_concept_saturation_axiom(
													ax->rhs,
													ax->lhs->successors[j]->fillers[k],
													ax->role->first_component_of_list[i], SUCCESSOR_LINK));
									pthread_mutex_unlock(&(ax->rhs->foreign_axioms_mutex));

									/*
									// push ax->rhs to the scheduled_concepts
									pthread_mutex_lock(&(scheduled_concepts_mutex));
									push(scheduled_concepts, ax->rhs);
									pthread_mutex_unlock(&(scheduled_concepts_mutex));
									*/

									// TODO: access to ax->rhs->successors should probably be synched!
									/*
									push(&(scheduled_concept->scheduled_axioms),
											create_concept_saturation_axiom(
													ax->lhs,
													ax->rhs->successors[j]->fillers[k],
													ax->role->first_component_of_list[i], PREDECESSOR_LINK));
													*/

								}
							}

					}

				}
				break;
			case SUCCESSOR_LINK:
				++saturation_total_link_count;
				if(add_successor(ax->lhs, ax->role, ax->rhs, tbox)) {
					// pthread_mutex_lock(&(ax->rhs->predecessors_mutex));
					// add_predecessor(ax->rhs, ax->role, ax->lhs, tbox);
					// pthread_mutex_unlock(&(ax->rhs->predecessors_mutex));

					++saturation_unique_link_count;

					// printf("LINK:");
					// print_concept(ax->lhs);
					// printf("->");
					// print_role(ax->role);
					// printf("->");
					// print_concept(ax->rhs);
					// printf("\n");

					int i, j, k;


					/*
					 * moved to PREDECESSOR_LINK
					// existential introduction
					for (i = 0; i < ax->rhs->subsumer_count; ++i)
						for (j = 0; j < ax->role->subsumer_count; ++j) {
							// TODO: the access to subsumer_list should probably be synched. !
							Concept* ex = GET_NEGATIVE_EXISTS(ax->rhs->subsumer_list[i], ax->role->subsumer_list[j]);
							if (ex != NULL)
								push(&(scheduled_concept->scheduled_axioms), create_concept_saturation_axiom(ax->lhs, ex, NULL, SUBSUMPTION_EXISTENTIAL_INTRODUCTION));
						}
					 */


					// the role chain rule
					// the role composition where this role appears as the second component
					for (i = 0; i < ax->role->second_component_of_count; ++i) {

					 // printf("role composition where this role appears as the second component: ");
					 // print_role(ax->role->subsumer_list[i]->second_component_of_list[j]);
					 // printf("\n");

						for (j = 0; j < ax->lhs->predecessor_r_count; ++j)
							if (ax->lhs->predecessors[j]->role == ax->role->second_component_of_list[i]->description.role_composition->role1) {
								for (k = 0; k < ax->lhs->predecessors[j]->filler_count; ++k) {
									pthread_mutex_lock(&(ax->lhs->predecessors[j]->fillers[k]->foreign_axioms_mutex));
									push(&(ax->lhs->predecessors[j]->fillers[k]->foreign_axioms),
											create_concept_saturation_axiom(
													ax->lhs->predecessors[j]->fillers[k],
													ax->rhs,
													ax->role->second_component_of_list[i], SUCCESSOR_LINK));
									pthread_mutex_unlock(&(ax->lhs->predecessors[j]->fillers[k]->foreign_axioms_mutex));

									/*
									// push ax->lhs->predecessors[j]->fillers[k] to the scheduled_concepts
									pthread_mutex_lock(&(scheduled_concepts_mutex));
									push(scheduled_concepts, ax->lhs->predecessors[j]->fillers[k]);
									pthread_mutex_unlock(&(scheduled_concepts_mutex));
									*/

									pthread_mutex_lock(&(ax->rhs->foreign_axioms_mutex));
									push(&(ax->rhs->foreign_axioms),
											create_concept_saturation_axiom(
													ax->rhs,
													ax->lhs->predecessors[j]->fillers[k],
													ax->role->second_component_of_list[i], PREDECESSOR_LINK));
									pthread_mutex_unlock(&(ax->rhs->foreign_axioms_mutex));

									/*
									// push ax->rhs to the scheduled_concepts
									pthread_mutex_lock(&(scheduled_concepts_mutex));
									push(scheduled_concepts, ax->rhs);
									pthread_mutex_unlock(&(scheduled_concepts_mutex));
									*/

								}
							}
					}


					/*
					 * moved to PREDECESSOR_LINK
					// now the same for the successors of the filler of the existential on the rhs
					// the role composition where this role appears as the first component
					for (i = 0; i < ax->role->first_component_of_count; ++i) {

						// printf("role composition where this role appears as the first component: ");
						// print_role(ax->rhs->description.exists->role->subsumer_list[i]->first_component_of_list[j]);
						// printf("\n");

						for (j = 0; j < ax->rhs->successor_r_count; ++j)
							if (ax->rhs->successors[j]->role == ax->role->first_component_of_list[i]->description.role_composition->role2) {
								// TODO: access to ax->rhs->successors should probably be synched!
								for (k = 0; k < ax->rhs->successors[j]->filler_count; ++k) {
									push(&(scheduled_concept->scheduled_axioms),
											create_concept_saturation_axiom(
													ax->lhs,
													ax->rhs->successors[j]->fillers[k],
													ax->role->first_component_of_list[i], SUCCESSOR_LINK));

								}
							}

					}
					*/


					// init
					pthread_mutex_lock(&(ax->rhs->foreign_axioms_mutex));
					push(&(ax->rhs->foreign_axioms), create_concept_saturation_axiom(ax->rhs, ax->rhs, NULL, SUBSUMPTION_INITIALIZATION));
					pthread_mutex_unlock(&(ax->rhs->foreign_axioms_mutex));

					/*
					// push ax->rhs to the scheduled_concepts
					pthread_mutex_lock(&(scheduled_concepts_mutex));
					push(scheduled_concepts, ax->rhs);
					pthread_mutex_unlock(&(scheduled_concepts_mutex));
					*/

				}
				break;
			default:
				fprintf(stderr, "Unknown saturation axiom type:%d, aborting.", ax->type);
				exit(EXIT_FAILURE);
			}
			free(ax);

			// first pop from the scheduled axioms
			ax = pop(&(scheduled_concept->scheduled_axioms));
			// if there is no scheduled axiom, pop from the foreign axioms
			if (ax == NULL) {
				pthread_mutex_lock(&(scheduled_concept->foreign_axioms_mutex));
				ax = pop(&(scheduled_concept->foreign_axioms));
				pthread_mutex_unlock(&(scheduled_concept->foreign_axioms_mutex));
			}

		}

		pthread_mutex_lock(&(scheduled_concepts_mutex));
		scheduled_concept = pop(scheduled_concepts);
		if (scheduled_concept != NULL)
			scheduled_concept->is_scheduled = 0;
		pthread_mutex_unlock(&(scheduled_concepts_mutex));
	}

	// printf("Total subsumptions:%d\nUnique subsumptions:%d\n", saturation_total_subsumption_count, saturation_unique_subsumption_count);
	// printf("Total links:%d\nUnique links:%d\n", saturation_total_link_count, saturation_unique_link_count);

	printf("Saturation worker finished: %lu\n", pthread_self());
	// printf("Thread 0x%.8x %.8x finished\n", pthread_getthreadid_np());

	pthread_exit((void*) 0);
	// return (void*) 0;
}
